package gov.nasa.jpf.symbc.modelcounter.latte;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.symbc.modelcounter.ModelCounter;
import gov.nasa.jpf.symbc.numeric.PathCondition;

import java.util.Set;

import org.apfloat.Apfloat;
import org.apfloat.Apint;

import za.ac.sun.cs.solver.expr.IntVariable;
import za.ac.sun.cs.solver.expr.Variable;

/**
 * A model counter that makes use of LattE (http://www.math.ucdavis.edu/~latte/).
 */
public class LattECounter extends ModelCounter {
	
	/*
	 * APfloat precision is set here
	 */
	private static final int PRECISION = 500;
	
	/**
	 * Constructor that instantiates the visitor.
	 */
	public LattECounter(Config config) {
		super(config);
	}
	
	/**
	 * Calculate the conditional probability of pathCondition relative to the preceding path's probability.
	 * 
	 * (non-Javadoc)
	 * @see gov.nasa.jpf.symbc.modelcounter.ModelCounter#getProbability(gov.nasa.jpf.symbc.numeric.PathCondition)
	 */
	@Override
	public Apfloat getConditionalProbability(PathCondition pathCondition, Apfloat parentProb) {
		Apint count = pathCondition.getInstance().countSolutions();
		Apint totalCount = Apint.ONE;
		Apfloat conditionalProb = Apfloat.ZERO;
		// use the per-variable ranges if available
		for(Variable v : pathCondition.getInstance().getAllVariables()) {
			IntVariable w = (IntVariable) v;
			Apint upper = new Apint(w.getUpperBound());
			Apint lower = new Apint(w.getLowerBound());
			totalCount = totalCount.multiply(upper.subtract(lower).add(Apint.ONE));
		}
		if (count.compareTo(Apint.ZERO) > 0) {
			conditionalProb = count.precision(PRECISION).divide(totalCount.precision(PRECISION));
			conditionalProb = conditionalProb.divide(parentProb);
		}
		try {
		assert conditionalProb.compareTo(Apfloat.ZERO) >=0 && conditionalProb.compareTo(Apfloat.ONE) <= 0:
			"condprob = " + conditionalProb + " parentProb = " + parentProb + " count = " + count + " total = " + totalCount;
		} catch (AssertionError ae) {
			System.out.println(ae.getMessage());
			conditionalProb = new Apfloat(1.0,PRECISION);
		}
		return conditionalProb;
	}

	/**
	 * Calculate the probability of the disjunction of a set of pathCondition.
	 */
	public Apfloat getProbability(Set<PathCondition> pathConditions) {
		return Apfloat.ZERO;
	}
	
}
